%replaceit: replace all ctxms from X1 by X2 in X3, return X4
replaceit(ORIG,RET,X,RET) :- member(X,ORIG), !.
replaceit(_,_,X,X) :- X=ctxm(_,_,_,_,_).
replaceit(_,_,[],[]).
replaceit(ORIG,RET,[X1|LST1],[X2|LST2]) :- replaceit(ORIG,RET,X1,X2), replaceit(ORIG,RET,LST1,LST2).
replaceit(ORIG,RET,pri(T,LST1),pri(T,LST2)) :- replaceit(ORIG,RET,LST1,LST2).

tocnt(ctxm(_,_,_,_,C),C).
tocnt([],[]).
tocnt([X1|LST1],[X2|LST2]) :- tocnt(X1,X2), tocnt(LST1,LST2).
tocnt(pri(T,LST1),pri(T,LST2)) :- tocnt(LST1,LST2).

% ----- printing messages -----------------------------------------------------

repl(Old, New, Orig, Replaced) :-
    atomic_list_concat(Split, Old, Orig),
    atomic_list_concat(Split, New, Replaced).

printa(ss(A,B)) :- !, print('ss'), printa(A), printa(B). % HACK FOR IDM CASE STUDY
printa((A,B)) :- !, printa(A), printa(B).
printa(X) :- string_to_atom(S1,X), repl('_','U',S1,S2), repl(',','C',S2,S3), print(S3).

printas([X]) :- !, printa(X).
printas([X|LST]) :- printa(X), print(','), printas(LST).

printmsgsc(LST) :- printmsgsc(LST,1).

printmsgsc([M],N) :- print('w'),print(N),print('='),printmc(M), !.
printmsgsc([M|REST],N) :- print('w'),print(N),print('='),printmc(M),print(','),NP1 is N+1,printmsgsc(REST,NP1).

printl([X]) :- printmc(X), !.
printl([X|LST]) :- print('pair('), printmc(X), print(','), printl(LST), print(')').

printmc([X]) :- printmc(X), !.
printmc([X|LST]) :- printmc(X),print(','),printmc(LST), !.
%printmc(pri(lst,LST)) :- length(LST,N),print('lst'),print(N),print('('),printmc(LST),print(')'), !.
printmc(pri(lst,[])) :- print('*** ERROR: empty lists not supported in equational model'), exit(2), !.
printmc(pri(lst,[_])) :- print('*** ERROR: length-1 lists not supported in equational model'), exit(2), !.
printmc(pri(lst,LST)) :- printl(LST), !.
printmc(pri(T,LST)) :- print(T),print('('),printmc(LST),print(')'), !.
printmc(X) :- printa(X).

noprim(pri(_,_)) :- !, fail.
noprim(_).

% ----- printing signature ----------------------------------------------------

max([X],X).
max([X|Xs],X):- max(Xs,Y), X >=Y.
max([X|Xs],N):- max(Xs,N), N > X.

printww(0) :- !.
printww(N) :- NM1 is N-1, printww(NM1), print('w'),print(N),print(',').

print_variables(LST) :-
  print('names '),
  % variables for message names
  findall(LEN,(member(FR,LST),length(FR,LEN)),ALLEN),max(ALLEN,MAXLEN),printww(MAXLEN),
  % variables occuring in frames
  findall(X,(member(FR,LST),member(MSG,FR),contains(MSG,X),noprim(X)),LSTX),list_to_set(LSTX,SETX),
  printas(SETX),print(';\n').

print_signature(QS) :- open('framework/signature', read, Input), process_sigfile(QS,Input), close(Input), !.
process_sigfile(QS,Input) :- 
  read_line_to_codes(Input,Codes),
  Codes \= end_of_file,
  !, sigfile_line(QS,Codes),
  process_sigfile(QS,Input).
process_sigfile(_,_) :- !.

sigfile_line(QS,[46]) :- print_variables(QS). % line with single dot
sigfile_line(_,Codes) :- format('~s', [Codes]), print('\n').

% ----- print frames ----------------------------------------------------------

print_frame(FR,IX) :-
  findall(X,(member(MSG,FR),contains(MSG,X),noprim(X)),LSTX),list_to_set(LSTX,SETX),
  print('   phi'),print(IX),print(' = new '),printas(SETX),print('.{'),
  printmsgsc(FR),
  print('}').
  
print_frames(LST) :- print_frames(LST,1).

print_frames([FR],IX) :- !, print_frame(FR,IX), print(';\n').

print_frames([X|FR],IX) :- print_frame(X,IX), print(',\n'), IXP1 is IX+1, print_frames(FR,IXP1).

% ----- print questions -------------------------------------------------------

print_framename(FRAMES,FRAME) :- print_framename(1,FRAMES,FRAME).
print_framename(N,[X|_],X) :- print('phi'), print(N), !.
print_framename(N,[_|LST],X) :- NP1 is N+1, print_framename(NP1,LST,X).

print_question(FRAMES,der(F,M)) :-
  print('  deducible '), printa(M), print(' '), print_framename(FRAMES,F).

print_question(FRAMES,nse(F1,F2)) :-
  print('  equiv '), print_framename(FRAMES,F1), print(' '), print_framename(FRAMES,F2).

print_questions(FRAMES,[X]) :- !,
  print_question(FRAMES,X), print(';\n').

print_questions(FRAMES,[X|LST]) :-
  print_question(FRAMES,X), print(',\n'),
  print_questions(FRAMES,LST).


% ----- print & run total kiss script -----------------------------------------------

printqs(L) :-
  % index all frames
  findall(FR,member(der(FR,_),L),LST1),
  findall(FR,member(nse(FR,_),L),LST2),
  findall(FR,member(nse(_,FR),L),LST3),
  append([LST1,LST2,LST3],LST),
  list_to_set(LST,FRAMES),

  % signature
  print_signature(FRAMES),

  % frames
  print('frames\n'), 
  print_frames(FRAMES),

  % print queries
  print('questions\n'),
  print_questions(FRAMES, L).

printqs_file(F,L) :- telling(X), open(F,write,OutF), tell(OutF), printqs(L), close(OutF), tell(X).

testresultq(1) :- !.
testresultq(2) :- !, fail.
testresultq(_) :- telling(X),tell(user_error),print('*** Failed to run KISS!\n'),tell(X), fail.

runq(Q) :-
  printqs_file('.experiment_pl_tmp',Q),
  shell('cat .experiment_pl_tmp | ./kiss | python framework/interpret1.py', RET),
  testresultq(RET).

% ----- detectability ---------------------------------------------------------

% for detectability of item D: require non-static equivalence for every
% subset of the set of all context items
detectableq(A,D,L) :-
  D=ctxm(_,_,_,_,CD),
  % findall items CE to D
  findall(X,(know(A,Y),contains(Y,X),ce(X,D)),LST),list_to_set(LST,SET), 
  % take all non-empty subsets of these items, including D
  findall(X,(subsets(SET,X),X\=[],member(D,X)),ALLSUB), %

  findall(M,know(A,M),ALLM1),
  tocnt(ALLM1,ALLM1C),
  append(ALLM1,[ctxm(a,a,a,a,CD)],ALLM),
  tocnt(ALLM,ALLMC),
  
  % non-static equivalence to original of any subset w/D replaced by guess
  findall(nse(ALLMC,ALLM2C),(member(X,ALLSUB),
                             replaceit(X,ctxm(a,a,a,a,guess),ALLM,ALLM2),
                             tocnt(ALLM2,ALLM2C)),L1),
  % derivability of the contents
  append(L1,[der(ALLM1C,CD)],L).

testdetect(A,D) :-
  detectableq(A,D,L),
  runq(L).


% ----- linkability -----------------------------------------------------------

relctxit2(_,LST,_,[],LST) :- !.

relctxit2(A,LST,IDS,NEWCX,RET) :-
  append(LST,NEWCX,ALLCX),
  findall(I,(know(A,Y),contains(Y,X),X=ctxm(D,P,_,I,I),member(ctx(D,P),NEWCX)),ALLI),
  append(IDS,ALLI,LSTI),
  list_to_set(LSTI,SETI),
  relctxit(A,ALLCX,SETI,RET).

% given list of contexts L, list of ids in contexts L: recursively find all contexts LSTN that are related by an identifier with contexts in L
relctxit(A,LST1,IDS,LSTN) :-
  findall(CX,(know(A,Y),contains(Y,X),X=ctxm(D,P,_,I,I),member(I,IDS),CX=ctx(D,P)),LCX), list_to_set(LCX,SCX), % find all context with a common identifier
  subtract(SCX,LST1,NEWCX),
  relctxit2(A,SCX,IDS,NEWCX,LSTN).

relctx(A,CTXS,RET) :-
  findall(I,(know(A,Y),contains(Y,X),X=ctxm(D,P,_,I,I),member(ctx(D,P),CTXS)),LSTI),
  list_to_set(LSTI,SETI),
  relctxit(A,CTXS,SETI,RET).

replaceioi(I,CS,ALLY,ALLYP,N) :-
  atom_concat(ioi,N,SIOI),
  findall(X,(member(Z,ALLY),contains(Z,X),X=ctxm(D,P,_,I,I),member(ctx(D,P),CS)),ALLX),
  replaceit(ALLX,ctxm(a,a,a,a,SIOI),ALLY,ALLYP).

replaceiois(ISET,CS,ALLY,ALLYP) :- replaceiois(ISET,CS,ALLY,ALLYP,1).

replaceiois([X],CS,ALLY,ALLYP,N) :- replaceioi(X,CS,ALLY,ALLYP,N), !.
replaceiois([X|LST],CS,ALLY,ALLYPP,N) :- replaceioi(X,CS,ALLY,ALLYP,N), NP1 is N+1, replaceiois(LST,CS,ALLYP,ALLYPP,NP1).

frameid(A,KBC,CS,Q) :-
  findall(I,(know(A,Y),contains(Y,ctxm(D,P,_,I,I)),member(ctx(D,P),CS)),ILST),list_to_set(ILST,ISET),
  findall(Y,know(A,Y),ALLY),
  replaceiois(ISET,CS,ALLY,ALLYP),
  tocnt(ALLYP,ALLYPC),
  Q=nse(KBC,ALLYPC).

linkableq(A,C1,C2,ALLQ) :-
   findall(YC,(know(A,Y),tocnt(Y,YC)),KBC),
   relctx(A,[C1,C2],SET0), subtract(SET0,[C1,C2],SET),
   findall(Q,(subsets(SET,X),frameid(A,KBC,[C1|X],Q)),ALLQ).


testlink(A,C1,C2) :-
  linkableq(A,C1,C2,Q),
  runq(Q).


findlinks(_,X,[],[X]).
findlinks(A,X,[Y|LST],[Y|RET]) :- testlink(A,X,Y), !, findlinks(A,X,LST,RET).
findlinks(A,X,[_|LST],RET) :- findlinks(A,X,LST,RET).

linkablepart2(_,[],[]).
linkablepart2(A,[X|LST],[RET1|RET2]) :-
  findlinks(A,X,LST,RET1),
  print('link('),print(A),print(','),sort(RET1,RET1S),print(RET1S),print(').\n'),
  subtract([X|LST],RET1,REST),
  linkablepart2(A,REST,RET2).




% old stuff

zipnum(_,[],[]).
zipnum(N,[X|LST],[(N,X)|LSTP]) :- NP1 is N+1, zipnum(NP1,LST,LSTP).



% primtm(X,D): print message X, replacing all ctxm(_,_,_,_,_) in D by 'ioi

printm(X,D) :- member(X,D), print('ioi'), !.
printm(ctxm(_,_,_,_,C),_) :- printa(C), !.
printm(pri(lst,[]),_) :- print('naught'), !.
printm([X],D) :- printm(X,D), !.
printm([X|LST],D) :- printm(X,D),print(','),printm(LST,D), !.
%printm(pri(lst,LST),D) :- printml(LST,D), !.
printm(pri(lst,LST),D) :- length(LST,N),print('lst'),print(N),print('('),printm(LST,D),print(')'), !.
printm(pri(T,LST),D) :- print(T),print('('),printm(LST,D),print(')'), !.
printm(X,_) :- print('** Unhandeled '), print(X).

% printmsgs([(N,M),D]): print w1=m1,...,wn=mn by recursively calling printm

printmsgs([],_) :- !.
printmsgs([(N,Y)],D) :- print('w'),print(N),print('='),printm(Y,D), !.
printmsgs([(N,Y)|REST],D) :- print('w'),print(N),print('='),printm(Y,D),print(','),printmsgs(REST,D).

% printframep: given actor A, frame name FN, set D of context items to be replaced by ioi,
%              context item CN: print frame containing knowledge of actor A in which all
%              items of D are replaced by 'ioi', and CN is included at the end

printframep(A,FN,D,CN) :-
  findall(ctxm(a,a,a,a,C),(know(A,Y),contains(Y,CP),CP=ctxm(_,_,_,_,C)),ALLC1),
  findall(ctxm(a,a,a,a,C),(contains(CN,CP),CP=ctxm(_,_,_,_,C)),ALLC2),
  append(ALLC1,ALLC2,ALLC), 
  list_to_set(ALLC,ALLCS), % all contents of items in knowledge base and CN
  print('   phi'),print(FN),print(' = new '),printm(ALLCS,D),print(',ioi.{'),
  findall(Y,know(A,Y),ALLY1),append(ALLY1,[CN],ALLY),
  zipnum(1,ALLY,ALLYN),
  printmsgs(ALLYN,D),
  print('},\n').

% printframe: given actor A, print frame 'phi' containing A's knowledge

printframe(A) :-
  findall(ctxm(a,a,a,a,C),(know(A,Y),contains(Y,CP),CP=ctxm(_,_,_,_,C)),ALLC),list_to_set(ALLC,ALLCS),
  print('   phi = new  '),printm(ALLCS,[]),print('.{'),
  findall(Y,know(A,Y),ALLY),
  zipnum(1,ALLY,ALLYN),
  printmsgs(ALLYN,[]),
  print('};\n').

% print frames for verifying detectability of d

printequivs(0,_) :- !.
printequivs(N,S) :-
  NM1 is N-1,
  printequivs(NM1,S),
  print('   equiv '), print(S), print(' phi'), print(N), print(',\n').

printframes(A,D) :-
  D=ctxm(_,_,_,_,CD),
  findall(X,(know(A,Y),contains(Y,X),ce(X,D),X\=D),LST),list_to_set(LST,SET),
  findall(X,subsets(SET,X),ALLSUB), zipnum(1,ALLSUB,ALLSUBN),
  printframep(A,0,[],ctxm(a,a,a,a,CD)),
  forall(member((N,X),ALLSUBN),printframep(A,N,[D|X],ctxm(a,a,a,a,CD))),
  printframe(A).


printquestions(A,D) :-
  D=ctxm(_,_,_,_,CD),
  findall(X,(know(A,Y),contains(Y,X),ce(X,D),X\=D),LST),list_to_set(LST,SET),
  findall(X,subsets(SET,X),ALLSUB),
  length(ALLSUB,L),
  printequivs(L, 'phi0'),
  print('   deducible '),printa(CD),print(' phi;\n').

printframesce(A,MP,C1,C2) :-
findall(X,(know(A,Y),contains(Y,X),ce(X,C1),X\=C1,X\=C2),LST1),
  findall(X,(contains(MP,X),ce(X,C1),X\=C1,X\=C2),LST2),
  append(LST1,LST2,LST),
  list_to_set(LST,SET), % SET contains all items in the knowledge base and additional message, apart from C1 and C2, that are content equivalent to them
  findall(X,nesub(X,SET),ALLSUB), zipnum(1,ALLSUB,ALLSUBN),
  printframep(A,0,[],MP),
  forall(member((N,X),ALLSUBN),printframep(A,N,[C1|X],MP)),
  printframe(A).

printquestionsce(A,MP,C1,C2) :-
  findall(X,(know(A,Y),contains(Y,X),ce(X,C1),X\=C1,X\=C2),LST1),
  findall(X,(contains(MP,X),ce(X,C1),X\=C1,X\=C2),LST2),
  append(LST1,LST2,LST),
  list_to_set(LST,SET), % SET contains all items in the knowledge base and additional message, apart from C1 and C2, that are content equivalent to them
  findall(X,nesub(X,SET),ALLSUB),
  length(ALLSUB,L),
  printequivs(L, 'phi0'),
  print('   deducible phi0 ok;\n').

printml(X,CS,D) :- X=ctxm(DM,P,_,I,I), member(ctx(DM,P),CS), member((N,I),D), print('ioi'), print(N), !.
printml(ctxm(_,_,_,_,C),_,_) :- printa(C), !.
printml(pri(lst,[]),_,_) :- print('naught'), !.
printml([X],CS,D) :- printml(X,CS,D), !.
printml([X|LST],CS,D) :- printml(X,CS,D),print(','),printml(LST,CS,D), !.
printml(pri(lst,LST),CS,D) :- length(LST,N),print('lst'),print(N),print('('),printml(LST,CS,D),print(')'), !.
printml(pri(T,LST),CS,D) :- print(T),print('('),printml(LST,CS,D),print(')'), !.
printml(X,_,_) :- print('** Unhandeled '), print(X).

printmsgsl([],_,_) :- !.
printmsgsl([(N,Y)],CS,D) :- print('w'),print(N),print('='),printml(Y,CS,D), !.
printmsgsl([(N,Y)|REST],CS,D) :- print('w'),print(N),print('='),printml(Y,CS,D),print(','),printmsgsl(REST,CS,D).

printframel(A,FN,CS) :-
  findall(ctxm(a,a,a,a,C),(know(A,Y),contains(Y,CP),CP=ctxm(_,_,_,_,C)),ALLC),list_to_set(ALLC,ALLCS),
  findall(I,(know(A,Y),contains(Y,ctxm(D,P,_,I,I)),member(ctx(D,P),CS)),ILST),list_to_set(ILST,ISET),
  zipnum(1,ISET,IOIS),
  findall(ctxm(a,a,a,a,X),(member((N,_),IOIS),atom_concat(ioi,N,X)),IOIL),
  append(ALLCS,IOIL,ALLNM),
  print('   phi'),print(FN),print(' = new '),printm(ALLNM,[]),print('.{'),
  findall(Y,know(A,Y),ALLY),
  zipnum(1,ALLY,ALLYN),
  printmsgsl(ALLYN,CS,IOIS),
  print('},\n').





printframesl(A,C1,C2) :-
  relctx(A,[C1,C2],SET0), subtract(SET0,[C1,C2],SET),
  %findall(CX,(know(A,Y),contains(Y,X),X=ctxm(D,P,_,_,_),CX=ctx(D,P),CX\=C1,CX\=C2),LST),list_to_set(LST,SET),
  findall(X,subsets(SET,X),ALLSUB), zipnum(1,ALLSUB,ALLSUBN),
  forall(member((N,X),ALLSUBN),printframel(A,N,[C1|X])),
  printframe(A).

printquestionsl(A,C1,C2) :-
  relctx(A,[C1,C2],SET0), subtract(SET0,[C1,C2],SET),
  findall(X,subsets(SET,X),ALLSUB),
  length(ALLSUB,L),
  printequivs(L, 'phi'),
  print('   equiv phi phi1;').


printalll(A,C1,C2) :-
  relctx(A,[C1,C2],CTXS), findall(I,(know(A,Y),contains(Y,X),X=ctxm(D,P,_,I,I),member(ctx(D,P),CTXS)),LSTI), list_to_set(LSTI,SETI), length(SETI,LEN),
  printsig(A,LEN),
  print('frames\n'),
  printframesl(A,C1,C2),
  print('questions\n'),
  printquestionsl(A,C1,C2).


printall(A,D) :-
  printsig(A,0),
  print('frames\n'),
  printframes(A,D),
  print('questions\n'),
  printquestions(A,D).


printderive(A,M) :-
  printsig(A,0),
  print('frames\n'),
  printframe(A),
  print('questions\n'),
  print('   deducible phi '),printm(M,[]),print(';\n').

printce(A,MP,C1,C2) :-
  printsig(A,0),
  print('frames\n'),
  printframesce(A,MP,C1,C2),
  print('questions\n'),
  printquestionsce(A,MP,C1,C2).

printws(0) :- !.
printws(ALLXL) :- ALLXLM1 is ALLXL-1, printws(ALLXLM1),print('w'),print(ALLXL),print(',').

printiois(0) :- print(',ioi'). 
printiois(1) :- print(',ioi1').
printiois(N) :- N>1, NM1 is N-1, printiois(NM1), print(',ioi'),print(N).

printvars(A,N) :-
  findall(ctxm(a,a,a,a,C),(know(A,Y),contains(Y,CP),CP=ctxm(_,_,_,_,C)),ALLC),list_to_set(ALLC,ALLCS),
  print('names '),
  findall(X,know(A,X),ALLX),length([x|ALLX],ALLXL),printws(ALLXL),
  printm(ALLCS,[]),
  printiois(N),
  print(';\n').

printsig(A,N) :- open('framework/signature', read, Input), process(A,N,Input), close(Input), !.
process(A,N,Input) :- 
  read_line_to_codes(Input,Codes),
  Codes \= end_of_file,
  !, handle_line(A,N,Codes),
  process(A,N,Input).
process(_,_,_) :- !.                                                              % catch-all

handle_line(A,N,[46]) :-printvars(A,N). % line with single dot
handle_line(_,_,Codes) :- format('~s', [Codes]), print('\n').

printallfile(A,D,F) :-
  telling(X),
  open(F,write,OutF),
  tell(OutF),
  printall(A,D),
  close(OutF),
  tell(X).

printalllfile(A,C1,C2,F) :-
  telling(X),
  open(F,write,OutF),
  tell(OutF),
  printalll(A,C1,C2),
  close(OutF),
  tell(X).

printderivefile(A,D,F) :-
  telling(X),
  open(F,write,OutF),
  tell(OutF),
  printderive(A,D),
  close(OutF),
  tell(X).

printcefile(A,MP,C1,C2,F) :-
  telling(X),
  open(F,write,OutF),
  tell(OutF),
  printce(A,MP,C1,C2),
  close(OutF),
  tell(X).

printallfiles(_,[],_).

printallfiles(A,[X|LST],N) :-
  atom_concat('kiss-', N, OUTF1),
  atom_concat(OUTF1, '.in', OUTF),
  print('Outputting '),print(OUTF),print(': detectability of '),print(X),print('\n'),
  printallfile(A,X,OUTF),
  NP1 is N+1,
  printallfiles(A,LST,NP1).

printallfiles(A) :-
  findall(Z,(know(A,Y),contains(Y,Z),Z=ctxm(_,P,_,_,_),P\=dot),LSTZ),list_to_set(LSTZ,SETZ),
  printallfiles(A,SETZ,1).


testresult(1) :- !.
testresult(2) :- !, fail.
testresult(_) :- telling(X),tell(user_error),print('*** Failed to run KISS!\n'),tell(X), fail.

testce(A,MP,C1,C2) :-
  printcefile(A,MP,C1,C2,'.experiment_pl_tmp'),
  shell('cat .experiment_pl_tmp | ./kiss | python framework/interpret1.py', RET),
  testresult(RET).

